COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.REQUIRE "HEAD.PUB[R,LES]" SOURCE
C00011 00003	.SS The First-Order Logic Solution
C00027 00004	.SS "Goals, Milestones, and Software"
C00042 00005	.CB Milestones
C00046 00006	.SS The Formal Reasoning Group.
C00049 00007	.bib
C00051 ENDMK
C⊗;
.REQUIRE "HEAD.PUB[R,LES]" SOURCE
.S FORMAL REASONING

\\pers John McCarthy, Richard Weyhrauch, William Glassmire, Michael Gordon,
Juan Bulnes, Robert Filman, Jerrold Ginsbarg, David Arnold, Arthur Thomas,
David Wilkins.

This includes the activities previously reported as proof-checking,
mathematical theory of computation, and representation theory.
They are combined in this proposal, because much the same people are
involved in all of them, and they require some of the same
developments of ideas and of software.

Before describing the present state of this work and what is
planned in the next eighteen months, we will explain our
conception of the problems involved in this area,
since this is perhaps the Laboratory's major
effort in the theoretical side of artificial intelligence.

.SS The Epistemological Part of Artificial Intelligence

Artificial intelligence has proved to be a very difficult scientific subject.
In the first ten years of AI research, the limits of what could be done by
straightforward programming on specific intellectual problems such as games
and theorem proving were explored.  Much effort was also invested in writing 
programs which "reason" about various areas of human knowledge.  Thus there 
is a large collection of problem solving programs, automatic programming 
systems, program verification systems, and so on.  Many of these programs 
represent clever and sophisticated solutions to specific problems; however, 
a formalization of a particular subject is generally not applicable 
to other domains.  In another direction, a number of ideas for general intelligent 
systems were explored, but with limited results.  
Once it became clear that computer systems of human intelligence level were
not going to be obtained in one grand rush, the general artificial intelligence 
problem was divided into subproblems which could be tackled separately.  In 
particular, the analysis of [McCarthy and Hayes] divides the problem into 
a %2heuristic%1 part and an %2epistemological%1 part.

The %2heuristic%1 part of the problem was studied first and is best understood.
It essentially involves methods of searching spaces of possibilities for the
solution to a problem.  The tendency of this work was to take whatever came 
easily to hand as the space of possibilities and concentrate on the search 
methods themselves.  However, it eventually became quite clear that in most 
classes of problems the barrier to approaching human performance lay in the
representation of information rather than in the search methods.  Moreover,
information relevant to a problem has to be taken in the form in which it 
can most easily be learned and then transformed into the most useful form 
for solving the problem.

Lately, therefore, the AI field has concentrated much of its attention on
what information an intelligent system needs and can get for its work and 
how to represent and to handle this information in the computer.  This is the
%2epistemological%1 part of the AI problem.  Since facts without techniques lead
nowhere and techniques without facts are meaningless, it seems essential to consider 
both the representation of information and the methods of reasoning whereby 
the solution to a problem follows from the facts.
  One way to study both 
questions is to build software to check human reasoning, in accord with the 
following principle, first stated in [McCarthy 1959]:

%3"In order for a program to be capable of learning something it must
first be capable of being told it."%1

The point is that whether a person or a computer program %2understands%1 the 
facts of a problem is in a sense independent of his problem solving ability; 
the question is whether he can follow, i.e. check, the correctness of the 
reasoning involved in the solution of the problem.  

At present the most difficult problem is to make
computers check common sense reasoning, a goal also
first posed in [McCarthy 1959].  Some results were reported in that
paper and in [McCarthy 1963] and [McCarthy and Hayes 1970].
However, no one has yet written a 
general purpose program to check the reasoning used by human beings in many
uncomplicated real-life situations.  At present there is no one program that
can even represent %3all%1 of the following problems:
.bc
   (a)	Decide how to travel from my home to the ARPA office in Washington.
taking into account the presence of information in travel agents, air line
personnel, telephone books, and signs at the airport.
   (b)  Learn to play a game by "reading" the rules
and take %2advice%1 from a human on strategy.
   (c)  Accept the facts about the motivations of buyers and sellers of
used cars.
   (d)  Accept even the most elementary facts of logistics or tactics.
.end

%3Because the common sense problem has proved very difficult and is vital for
artificial intelligence, it is important to try to split it
into subproblems that can be attacked separately%1.  We have already
mentioned the split into heuristic and epistemological parts.  
In this case the epistemological part can be further split into
the subproblems first, of discovering the facts of the common sense world
and second, of following deductive reasoning.

	The %3Formal Reasoning Group%1 is pursuing both of these objectives:
.SS The First-Order Logic Solution

The %3Formal Reasoning Group's%1 approach to the epistemological problem 
is based on first-order logic, 
by which we mean both the syntactic and semantic theory of the first order 
predicate calculus.  The predicate calculus is the language used in
the %2formal%1 systems mentioned above which are adequate to express
mathematical reasoning.  The semantic component of first-order logic
defines the correspondence between the grammatical constructs of the
formal systems and the mathematical objects they describe.  E.g., the
symbol "+" in a formal system is usually declared to correspond to ordinary
numerical addition.

We have written a program FOL which captures the computational part of 
first-order logic.  The basic grammar of FOL is 
modeled on the natural deduction representation of first order logic
set forth in [Prawitz 1965].  The semantic analysis is contained in a 
group of subroutines, collectively christened semantic attachment, which  
is a computational version of the correspondence between the grammar
and the things being reasoned about.  Semantic attachment, which permits 
interaction between the program and the real world, is perhaps the most 
innovative feature of FOL.  

To explain the relevance of first-order logic to the reasoning problem,
we discuss a collection of problems which we expect are within the 
capabilities of FOL.

One example is analysis of photographs and diagrams.  Consider in
particular an aerial photograph of a city.  Let us assume that
we have a tentative analysis of such a photograph, generated 
mechanically or by hand, which identifies certain picture elements
as trucks, streets, buildings, and so on.  One way to decide whether
this analysis corresponds to a certain model of the city is to use 
semantic attachment to match the elements of the picture with 
corresponding objects in the model.  In our conceptualization of
this problem the picture analysis is embedded in an appropriate
theory in the first-order predicate calculus, and the semantic
component of first-order logic is used to determine whether this
theory is consistent with the given model.  Inconsistency implies
that the theory, and hence the picture analysis, is incorrect.

We hope to formalize statements about programs that depend on 
facts about the physical world in FOL.  One
example is a program which operates on physical geometric objects 
and therefore needs to analyze their properties.
Semantic attachment will be used to express 
to the computer both facts about the shape and size of the 
objects involved and to define the purposes.  In one case,
the program might be asked to use two blocks, one 4 inches by
3 inches by 2 inches and a 2-inch cube, to build a structure
6 inches high.  A different question might be to determine whether
a triangle with sides 4 inches, 4 inches, and 7 inches fits 
inside a rectangle, 3 inches by 6 inches.

A question similar in spirit to the preceding is 
to verify a program when its statement of correctness depends on
knowing facts about the real world.  A simple example is that the
records of an airline reservation system should correspond 
to reality; that is, a customer which the program thinks has a 
reservation should actually have one,
and a command and control system's list of 
airplanes, with their characteristics and locations, should 
agree with actual characteristics and locations.  
A proof that such a program meets its 
specifications will involve expressing facts about the
real world.  

The latter examples show that programs of general interest may 
need a formalization of facts about the real world just to express 
(in a way understandable to a computer) their  correctness. 
It is problems like these that we would eventually 
like to treat easily.

What are FOL's present capabilities?  The following mathematical
problems have been partly or completely solved:
.bs
  (a)  The theorem "If p is a prime number and p divides the product a*b, 
       then p divides a or p divides b" has been proved.

  (b)  The theorem "If G is a finite group and S is a subgroup, then the
       order of S divides the order of G" has been proved.  This theorem
       involves expressing a significant part of set theory.

  (c)  The "ripple-carry" algorithm for base 2 addition has been 
       proved correct.

  (d)  Two chess problems whose solution requires reasoning more complex 
       than a case-by-case analysis are being formalized.
.end

Even in doing these simple problems, we have found a large difference
between the informal arguments understood by mathematicians and
the formal arguments strictly acceptable in first order logic.  This means
that mathematicians abbreviate more than they think they do, and FOL
has been modified to accept some of these abbreviated modes of reasoning
and will accept still more in the future.

The research applications of FOL fall in three separate areas.  The
most immediately accessible are the proofs in mathematics.  There
are several reasons for studying this problem. %2First%1, mathematics 
provides many easily available examples of long chains of 
human reasoning.  %2Second%1, the first-order logic representation 
of mathematics is the model on which FOL is based, 
so checking mathematical proofs is an obvious experimental
test.  %2Third%1, the formal notions used to represent mathematics are
well understood, so that correct axiomatizations for formalizing proofs
are easily obtained (though our experience shows that finding the most
usable axiomatization is still a problem).

The second area of applications is in correctness proofs, both for 
hardware implementations and for software.  There are three reasons 
for this: %2First%1, machine-checked correctness proofs are, in our 
opinion, the most promising practical technique in the long run for 
reducing the time necessary to get correct computer programs.  The 
reasons why this is so were elaborated in some of our earlier 
proposals to ARPA [Stanford 1969],
11d pursuing this approach has been one of the major tasks of our
ARPA contract.  As mentioned, we have proved the correctness
of the ripple-carry algorithm for base 2 addition, and we will soon
prove the correctness of other algorithms, specifically the 
look-ahead carry algorithm.  %2Second%1, this domain complements pure 
mathematics nicely as a test of our ability to formalize reasoning, 
because there is still a substantial conceptual problem of determining 
what the right axioms are.  %2Third%1, AI in general is concerned with
reasoning that a strategy will solve a problem, and strategies are a
kind of program.  Therefore, the mathematics of program correctness
is likely to play an essential role in artificial intelligence as a
whole. 

Finally, we are using FOL to experiment with common sense reasoning. 
To study the problem of combining deductive reasoning with the 
representation of basic common sense facts, one needs a domain in
which there is a clear division between facts and reasoning.  Such a 
domain is provided by the chess problems mentioned above, which combine 
the step-by-step deductive reasoning characteristic of mathematical 
logic with facts obtained by observing the chessboard.  For example,
the first step in solving one of the problems is to observe that Black 
is in check.  A human being does not "prove" that Black is in check from 
axioms giving the positions of all the pieces; rather we just look at 
the board and see that Black is in check.  In contrast, the nature of
the deductive reasoning involved is exemplified by another part of 
the same problem; one shows that a 
White rook is a promoted pawn, a fact that certainly is not obvious
from the board.  

The important consideration in this problem is not the
domain of chess but the attempt to isolate the way in which computation
interacts with deduction.  FOL's semantic attachment feature models our 
observational ability by introducing a correspondence between 
certain predicate and function symbols in the logic and certain 
computable LISP functions and predicates.  When a statement 
involving these function symbols applied to known constants 
occurs, it can be verified by direct calculation using the corresponding LISP 
functions.  In the case of chess, we call the collection of LISP functions 
%2the chess eye%1.  We have explored what these functions are, but we don't 
have anything like a complete collection yet, because even the domains that 
these functions ought to have is unclear.  For example, some of them give 
answers when the position is only partially specified, and this property is 
essential to their use.  Therefore, we need to work with some useful class of 
partially specified positions.

Already the chess example has showed us improvements to formal logic
required to represent reasoning that involves observation.  We are
now ready to extend this work to include observations of the physical
world with a television camera.  This will be harder because there is
a great problem in expressing what humans know about the world of
scenes in a form usable by a computer, i.e. as FOL axioms and
attachments.

.SS "Goals, Milestones, and Software"

At present, the general goal of the %3Formal Reasoning Group%1 is to  
find out how to make it easier to express a many kinds of problems, both
mathematical and non-mathematical, in FOL.  We want to increase the
expressive capability of the basic FOL language and to make the actual
proof-checking procedure simpler and easier to use.  One way of achieving
the former is to modify the grammer to include other constructs, e.g.
conditional terms.  The latter involves discovering and implementing 
more powerful rules of inference, e.g. subgoaling or decision proceedures
for particular domains.  As explained above this is an essential 
prerequisite to machines actually being able to find solutions to these 
problems in an effecttive but general way.  In the intermediate term
we will produce an interface which will allow other programs to use
the expressive and deductive powers of FOL as they see fit.

Over the past several months we have demonstrated that it is possible 
to express many varieties of reasoning in FOL.  However, in practice a 
formalized proof is longer and more complicated than the corresponding 
informal proof.  Work is now in progress analyzing the formal proofs 
that have been done.  The proofs we have in hand are:

.bs
  (a)  The theorem "If p is a prime number and p divides the product a*b, 
       then p divides a or p divides b".  This theorem requires a knowledge
       of arithmetic.

  (b)  The theorem "If G is a finite group and S is a subgroup, then the
       order of S divides the order of G".  This theorem and the next used
       a significant part of set theory.

  (c)  The theorem "Consider a countable infinity set of vertices, each 
       vertex being connected to every other by a thread, each thread being 
       red or black.  Prove that there is an infinite subset of these 
       vertices, such that the connecting threads within the subset are 
       all of the same color.

  (d)  The theorem "p is a prime then (p-1)!≡1(mod p)".  This is usually 
       called Wilson's theorem.

  (e)  A proof that a hardware implementation of the "ripple-carry" algorithm 
       for base 2 addition has been proved correct.

  (f)  Two chess problems whose solution requires reasoning more complex 
       than a case-by-case analysis are being formalized.
.end

These proofs are at least as complicted (and in most cases more complicated)
than any proofs previously formulated for a machine to handle.  They are,
with the exception of (e), far beyond the capabilities of present day 
theorem "provers".  We expect to extract from these examples information 
about how we should configure computer software to represent reasoning 
problems of this complexity.  The results of this examination will influence 
how some of the features below will be developed.  

One problem in AI has been how does a program examine itself.  Suppose
you ask yourself why you believe something and you answer because I 
have convinced myself that it is true, i.e. I have proved it.  In 
order to make sense of this remark you must have some idea about
what it means to you for something to be a convincing argument.  This
is like being able to explain what a proof is.  Logicians call the
theory which describes the proofs in some theory its metatheory.  It
is a fact that a large part of the mathematics as well as common
sense reasoning is more accurately described is metatheoretical.  For 
example, any description of how to look for proofs is a part of 
the metatheory.  Another example of a metamathematical 
concept is the common three-dot notation for sequences, e.g. x1, x2, 
 ... , xn.  Another example is describing axiom schemas.  In the past
most treatments of first-order predicate calculus have been in
resolution theorem provers.  Their inability to express axiom schemas,
i.e. to properly express the metatheory, has limited their capability
to do proofs of arithmetic or set theory and thus excluded much of 
mathematics.  To make FOL accept such reasoning requires formalizing 
its metatheory. We intend to add to FOL the ability to talk about its 
own proofs.  We refer to this as MFOL (for metaFOL).  

We will use MFOL to check some major metamathematics theorem of traditional
logic. At the moment we are considering Goedel's proof of the consistency
of the continuum hypothesis.  A word should perhaps be said here about
the value of this problem from ARPA's point of view.  
The overall objective of this work is to discover ways 
to represent reasoning using machines.  We believe that
the difficulties involved in representing deductive reasoning
will be the same for widely varying classes of problems, so
that it is primarily a matter of taste which problems we try 
to represent.  This particular problem is both difficult 
and representative.  We may never "finish" this project as we might 
learn all we think we can about building MFOL before its finished.

An especially important project is to represent in FOL the 
notions of set theory, which is the vehicle used by
first-order logic to express higher mathematics.  In
particular, set theory provides a framework for expressing
analysis, that branch of mathematics which includes 
trigonometry and the calculus.  A proof of the correctness
of a program for computing satellite trajectories (or more
simply, for computing sines and cosines) can only be expressed
in analysis.  There are several alternative axiomatizations
known for set theory, and part of this project is to choose
the most suitable for formalization in FOL.  

The above projects are designed to allow us to study theories,
i.e. formal systems, that at a theoretical (although not practical) 
level have well understood representations to study.  In addition we 
will investigate how these concepts actually work in areas for which 
the representation of knowledge or the reasoning that is done is still 
in question.  As mentioned above, chess problems have been an 
extremely useful vehicle for studying the interplay between formal 
proofs and the semantic attachment mechanism of FOL in a non-mathematical
area.  It should be pointed out that the use of chess was not for the
purpose of building software to play a game of chess, but rather to
study how proofs can be represented.  Thus it is a test case for more
real world applications of semantic attachment.  We will explore several 
aspects of the use of FOL in reasoning about the actual physical world --
the representations of physical structure, visual appearance, and some 
causal notions.  The semantic attachment feature will permit us
to connect the FOL reasoning mechanism with sensory 
apparatus (a TV camera). For example, a user may attach 
to an FOL term, representing the distance from one object 
to another, a vision program which can calculate the distance 
by examining a sequence of TV pictures.  We are presently
working on FOL axiomatizations for various geometries relevant 
to visual perception and visuo-motor tasks, e.g. projective 
geometry and the geometry of solids. Again, semantic attachment
will be utilized to define algebraic representations of geometric 
notions and use algebraic computations to supplement 
purely geometric reasoning.  We will also need to study 
how to translate the concepts of a geometry based on perceptions 
of space into classical Euclidean geometry of physical space.
The grand culmination will be a proof of the correctness of 
a strategy for a physical manipulation and assembly task.  
This differs from a practical assembly program in that
we are trying to express in a formal language much 
of the physical intuition which is at present 
coded into assembly programs in an ad hoc way.  

A form of Dana Scott's logic for computable functions will be axiomatized
in the predicate calculus in a form usable in FOL.  The proofs about 
programs which have been carried out in the specialized system LCF will 
thus be expressible in FOL.  Since LCF does not include quantification 
rules or set theoretic axioms, the FOL system will allow simpler proofs 
of more assertions.  

Michael Gordon's thesis describes a technique for proving 
implementations (programs) correct.  The basic idea is to
translate the (obvious) semantic equations defining the meaning
of the program into an operational model which permits 
correctness proofs by induction on the length of computations.
The language treated in the thesis was pure LISP, a subset
of LISP 1.5.  The correctness proofs obtained will be extended
to most of LISP 1.5.  Also, by analyzing these proofs, a 
formalism for expressing them will be developed and embedded in FOL.

A notion of abstract pattern that is a generalization of
linguistic patterns will be further developed and applied to 
chess temporal and spatial patterns.  This will develop our 
understanding of the patterns used in human reasoning.  We
shall also apply it to describing the relations among objects
on a table and their two dimensional projections in a TV camera
image.  
.CB Milestones

⊗ September 1975: Semantic attachment will be made compatible with the full 
many sorted logic of FOL.

⊗ October 1975: An experiment using semantic attachment together with a TV 
camera will be designed.

⊗ October 1975: A suitable axiomatization of set theory will be expressed in 
FOL.

⊗ October 1975: The correctness proofs for LISP 1.5 will be finished.

⊗ November 1975: A form of Dana Scott's logic for computable functions 
  will be axiomatized in the predicate calculus in a form usable in FOL.

⊗ January 1976: A notion of abstract pattern that is a generalization of
linguistic patterns will be developed and applied to temporal and spatial 
patterns.  

⊗ February 1976: An initial version of MFOL will be implemented.

⊗ August 1976: The representations of physical concepts discussed
above will be expressed in FOL.  An experiment using a TV camera 
together with FOL will be finished.

⊗ September 1976: Abstract patterns will be applied to describe
the relations among objects on a table and their two dimensional 
projections in a TV camera image.

.CB Software

To accomplish these goals will require several modifications and
additions to the present FOL software.  The code will be written
in pure LISP (easily translatable into INTERLISP) and available
for use at other sites on the ARPA net.  Several other researchers
have already expressed interest in using the program.

The following software will be completed during this contract:
.bc
⊗ The semantic attachment mechanism.  
⊗ A preliminary version of MFOL.
⊗ A method of specifying goals and creating subgoals.
⊗ A decision procedure for monadic predicate logic.
⊗ A rule of inference allowing convenient manipulation of quantifiers.
⊗ The ability of users to make definitions.
⊗ The ability of users to create theorems.
⊗ An interface of FOL to other LISP programs.
.end

These are not included in the section on milestones as the exact order
in which they will be done is not yet decided, so no specific dates 
could be assigned to most of them.
.SS The Formal Reasoning Group.

John McCarthy is Professor of Computer Science and has worked in the area
of formal reasoning applied to computer science and artificial intelligence
since 1957.
He is working on the translation of the Scott theory in FOL, on the expression
of chess reasoning in FOL, and on a formalism for generalized patterns again
using first order logic.

Richard Weyhrauch is Research Associate in Computer Science,
has a PhD from Stanford in mathematical logic and has worked on mathematical
theory of computation and the development of proof-checkers.  He is in charge
of the work on FOL.

Bill Glassmire is Research Associate in Computer Science,
has joined the group recently, is also a Stanford PhD in mathematical logic.
Weyhrauch and Glassmire are extending FOL and applying it to problems in
mathematics and mathematical theory of computation.

Michael Gordon has a PhD in computer science from the University of Edinburgh.
His thesis was on reasoning about a semantics and implementation of pure
LISP within the Scott-Strachey framework.
He will pursue the formalization of the interactive and machine oriented aspects
of LISP.

Arthur Thomas is a graduate student in psychology, has worked on FOL, and is
interested in application of FOL to reasoning about
projective geometry and to visually perceived scenes and other real world
phenomena.
Juan Bulnes is studying combinatorial proofs in FOL.
Robert Filman is working on expressing chess reasoning in FOL.
David Arnold is applying FOL to set theoretical problems.
David Wilkins is working on abstract patterns.
.bib

[McCarthy 1959] John McCarthy, "Programs with Common Sense", <Proc. Int. Conf.
on Mechanisation of Thought Processes>, Teddington, England, National Physical
Laboratory, 1959.

[McCarthy 1963] John McCarthy, "A Basis for a Mathematical Theory of Computation",
in  Biaffort, P., and Herschberg, D., (eds.), <Computer Programming and Formal
Systems,> North-Holland, Amsterdam, 1963.

[McCarthy and Hayes]  John McCarthy and Patrick Hayes, "Some Philosophical Problems from the
Standpoint of Artificial Intelligence", AIM-73, November 1968; also in
D. Michie (ed.), <Machine Intelligence,> American Elsevier, New York, 1969.

[Prawitz 1965] Dag Prawitz, <Natural Deduction,> Almqvist & Wiksell, Stockholm, 1965.

[Stanford 1969], Stanford University, "Proposal for Continuation of the
Stanford Artificial Intelligence Project and the Heuristic Dendral Project",
proposal to ARPA, June 1969.

.end